es:ES, T, C:Type, Out:AbsInterface(:C  T). abs-R   CE 

latex

Definitions

abs-R , e  X, x.A(x), A c B, , case b of inl(x) => s(x) | inr(y) => t(y), True, False, tt, ff, if b then t else f fi , E, t.1, x. t(x), X(e), AbsInterface(A), let x,y = A in B(x;y), ES, EqDecider(T), EOrderAxioms(E; pred?; info), IdLnk, type List, Msg(M), left + right, Unit, , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r  s, e < e', , Top, P & Q, x:A  B(x), Knd, kindcase(k; a.f(a); l,t.g(l;t) ), Type, constant_function(f;A;B), P  Q, A, b, s = t, <a, b>, loc(e), SWellFounded(R(x;y)), pred!(e;e'), x:A. B(x), t  T, x:AB(x), , Id, EState(T), f(a)

Lemmas

constant function wf, val-axiom wf, es-interface-val wf, pi1 wf, assert wf, bfalse wf, btrue wf, false wf, true wf, es-is-interface wf